{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds #-}

{-# OPTIONS_GHC -Wno-orphans #-}

{-| Pretty printer for the concrete syntax.
-}
module Agda.Syntax.Concrete.Pretty
  ( module Agda.Syntax.Concrete.Pretty
  , module Agda.Syntax.Concrete.Glyph
  ) where

import Prelude hiding ( null )

import Data.Maybe
import qualified Data.Foldable  as Fold
import qualified Data.Strict.Maybe as Strict

import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Glyph

import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List1 ( List1, (<|) )
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.List2 as List2
import Agda.Utils.Maybe
import Agda.Utils.Null
import qualified Agda.Syntax.Common.Aspect as Asp
import Agda.Syntax.Common.Pretty
import Agda.Interaction.Options ( HasOptions(pragmaOptions), optPolarity )

import Agda.Utils.Impossible

deriving instance Show Expr
deriving instance (Show a) => Show (OpApp a)
deriving instance Show Declaration
deriving instance Show Pattern
deriving instance Show a => Show (Binder' a)
deriving instance Show TypedBinding
deriving instance Show LamBinding
deriving instance Show BoundName
deriving instance Show ModuleAssignment
deriving instance Show Pragma
deriving instance Show RHS
deriving instance Show LHS
deriving instance Show LHSCore
deriving instance Show LamClause
deriving instance Show WhereClause
deriving instance Show ModuleApplication
deriving instance Show DoStmt
deriving instance Show Module

-- Lays out a list of documents [d₁, d₂, …] in the following way:
-- @
--   { d₁
--   ; d₂
--   ⋮
--   }
-- @
-- If the list is empty, then the notation @{}@ is used.

bracesAndSemicolons :: Foldable t => t Doc -> Doc
bracesAndSemicolons ts = case Fold.toList ts of
  []       -> "{}"
  (d : ds) -> sep (["{" <+> d] ++ map (";" <+>) ds ++ ["}"])

prettyTactic :: BoundName -> Doc -> Doc
prettyTactic = prettyTactic' . bnameTactic

prettyFiniteness :: BoundName -> Doc -> Doc
prettyFiniteness name
  | bnameIsFinite name = ("@finite" <+>)
  | otherwise = id

prettyTactic' :: TacticAttribute -> Doc -> Doc
prettyTactic' t = (pretty t <+>)

instance Pretty a => Pretty (TacticAttribute' a) where
  pretty (TacticAttribute t) =
    ifNull (pretty t) empty \ d -> "@" <> parens (hlKeyword "tactic" <+> d)

instance Pretty (ThingWithFixity Name) where
    pretty (ThingWithFixity n _) = pretty n

-- | Show the attributes necessary to recover a modality, in long-form
-- (e.g. using at-syntax rather than dots). For the default modality,
-- the result is at-ω (rather than the empty document). Suitable for
-- showing modalities outside of binders.
attributesForModality :: HasOptions m => Modality -> m Doc
attributesForModality mod@(Modality r q c p)
  | mod `elem` [defaultCheckModality, defaultModality] = do
      showPolarity <- optPolarity <$> pragmaOptions
      pure $ text "@ω" <+> if showPolarity then polarity else empty
  | otherwise = pure $ fsep $ catMaybes [relevance, quantity, cohesion, Just polarity]
  where
    relevance = case r of
      Relevant        {} -> Nothing
      Irrelevant      {} -> Just "@irrelevant"
      ShapeIrrelevant {} -> Just "@shape-irrelevant"
    quantity = case q of
      Quantity0{} -> Just "@0"
      Quantity1{} -> Just "@1"
      Quantityω{} -> Nothing
    cohesion = case c of
      Flat{}       -> Just "@♭"
      Continuous{} -> Nothing
      Squash{}     -> Just "@⊤"
    polarity = case modPolarityAnn p of
      MixedPolarity    -> "@mixed"
      Positive         -> "@+"
      Negative         -> "@-"
      StrictlyPositive -> "@++"
      UnusedPolarity   -> "@unused"

instance Pretty (OpApp Expr) where
  pretty (Ordinary e) = pretty e
  pretty (SyntaxBindingLambda r bs e) = pretty (Lam r bs e)

instance Pretty a => Pretty (MaybePlaceholder a) where
  pretty Placeholder{}       = "_"
  pretty (NoPlaceholder _ e) = pretty e

instance Pretty Expr where
    pretty = \case
            Ident x          -> pretty x
            KnownIdent nk x  -> annotate nk (pretty x)
            Lit _ l          -> pretty l
            QuestionMark _ n -> hlSymbol "?" <> maybe empty (text . show) n
            Underscore _ n   -> maybe underscore text n
            e@(App _ _ _)    ->
                case appView e of
                    AppView e1 args     ->
                        fsep $ pretty e1 : map pretty args
--                      sep [ pretty e1
--                          , nest 2 $ fsep $ map pretty args
--                          ]
            RawApp _ es    -> fsep $ map pretty $ List2.toList es
            OpApp _ q _ es         -> fsep $ prettyOpApp empty q es
            KnownOpApp nk _ q _ es -> fsep $ prettyOpApp nk q es

            WithApp _ e es -> fsep $
              pretty e <| fmap ((hlSymbol "|" <+>) . pretty) es

            HiddenArg _ e -> braces' $ pretty e
            InstanceArg _ e -> dbraces $ pretty e
            Lam _ bs (AbsurdLam _ h) -> lambda <+> fsep (fmap pretty bs) <+> absurd h
            Lam _ bs e ->
                sep [ lambda <+> fsep (fmap pretty bs) <+> arrow
                    , nest 2 $ pretty e
                    ]
            AbsurdLam _ h -> lambda <+> absurd h
            ExtendedLam _ e pes ->
              lambda <+>
              prettyErased e (bracesAndSemicolons (fmap pretty pes))
            Fun _ e1 e2 ->
                sep [ pretty (getModality e1) <+> pretty e1 <+> arrow
                    , pretty e2
                    ]
            Pi tel e ->
                sep [ pretty (Tel $ smashTel $ List1.toList tel) <+> arrow
                    , pretty e
                    ]
            Let _ ds me  ->
                sep [ hlKeyword "let" <+> vcat (fmap pretty ds)
                    , maybe empty (\ e -> hlKeyword "in" <+> pretty e) me
                    ]
            Paren _ e -> parens $ pretty e
            IdiomBrackets _ es ->
              case es of
                []   -> emptyIdiomBrkt
                [e]  -> leftIdiomBrkt <+> pretty e <+> rightIdiomBrkt
                e:es -> leftIdiomBrkt <+> pretty e <+> fsep (map (("|" <+>) . pretty) es) <+> rightIdiomBrkt
            DoBlock _ ss -> hlKeyword "do" <+> vcat (fmap pretty ss)
            As _ x e  -> pretty x <> hlSymbol "@" <> pretty e
            Dot _ e   -> hlSymbol "." <> pretty e
            DoubleDot _ e  -> hlSymbol ".." <> pretty e
            Absurd _  -> hlSymbol "()"
            Rec _ _ xs ->
              sep [hlKeyword "record", bracesAndSemicolons (map pretty xs)]
            RecUpdate _ _ e xs ->
              sep [hlKeyword "record" <+> pretty e, bracesAndSemicolons (map pretty xs)]
            RecWhere _ _ xs -> sep [hlKeyword "record" <+> hlKeyword "where", nest 2 (vcat $ map pretty xs)]
            RecUpdateWhere _ _ e xs -> sep [hlKeyword "record" <+> pretty e <+> hlKeyword "where", nest 2 (vcat $ map pretty xs)]
            Quote _     -> hlKeyword "quote"
            QuoteTerm _ -> hlKeyword "quoteTerm"
            Unquote _   -> hlKeyword "unquote"
            Tactic _ t -> hlKeyword "tactic" <+> pretty t
            -- Andreas, 2011-10-03 print irrelevant things as .(e)
            DontCare e -> hlSymbol "." <> parens (pretty e)
            Equal _ a b -> pretty a <+> equals <+> pretty b
            Ellipsis _  -> hlSymbol "..."
            Generalized e -> pretty e
        where
          absurd NotHidden  = parens mempty
          absurd Instance{} = dbraces mempty
          absurd Hidden     = braces mempty

instance (Pretty a, Pretty b) => Pretty (Either a b) where
  pretty = either pretty pretty

instance Pretty a => Pretty (FieldAssignment' a) where
  pretty (FieldAssignment x e) = sep [ pretty x <+> equals, nest 2 $ pretty e ]

instance Pretty ModuleAssignment where
  pretty (ModuleAssignment m es i) = fsep (pretty m : map pretty es) <+> pretty i

instance Pretty LamClause where
  pretty (LamClause ps rhs _) =
    sep [ fsep (map pretty ps)
        , nest 2 $ pretty' rhs
        ]
    where
      pretty' (RHS e)   = arrow <+> pretty e
      pretty' AbsurdRHS = empty

-- Andreas, 2024-02-25
-- Q: Can we always ignore the tactic and the finiteness here?
instance Pretty BoundName where
  pretty (BName x _fix _tac _fin) = pretty x

data NamedBinding = NamedBinding
  { withHiding   :: Bool
  , namedBinding :: NamedArg Binder
  }

isLabeled :: NamedArg Binder -> Maybe ArgName
isLabeled x
  | visible x              = Nothing  -- Ignore labels on visible arguments
  | Just l <- bareNameOf x = boolToMaybe (l /= nameToRawName (boundName $ binderName $ namedArg x)) l
  | otherwise              = Nothing

instance Pretty a => Pretty (Binder' a) where
  pretty (Binder mpat UserBinderName n) =
    applyWhenJust mpat (\ pat -> (<+> ("@" <+> parens (pretty pat)))) $ pretty n

  pretty (Binder pat InsertedBinderName n) = case pat of
    Just pat -> parens (pretty pat)
    Nothing  -> pretty n

instance Pretty NamedBinding where
  pretty (NamedBinding withH
           x@(Arg (ArgInfo h (Modality r q c p) _o _fv (Annotation lock))
               (Named _mn xb@(Binder _mp _ (BName _y _fix t _fin))))) =
    applyWhen withH prH $
    applyWhenJust (isLabeled x) (\ l -> (text l <+>) . (equals <+>)) (pretty xb)
      -- isLabeled looks at _mn and _y
      -- pretty xb prints also the pattern _mp
    where
    prH = prettyRelevance r
        . prettyHiding h mparens
        . (coh <+>)
        . (qnt <+>)
        . (pol <+>)
        . (lck <+>)
        . (tac <+>)
    coh = pretty c
    qnt = pretty q
    pol = pretty p
    tac = pretty t
    lck = pretty lock
    -- Parentheses are needed when an attribute @... is printed
    mparens = applyUnless (null coh && null qnt && null lck && null tac && null pol) parens

instance Pretty LamBinding where
    pretty (DomainFree x) = pretty (NamedBinding True x)
    pretty (DomainFull b) = pretty b

instance Pretty TypedBinding where
    pretty (TLet _ ds) = parens $ hlKeyword "let" <+> vcat (fmap pretty ds)
    pretty (TBind _ xs (Underscore _ Nothing)) =
      fsep (fmap (pretty . NamedBinding True) xs)
    pretty (TBind _ xs e) = fsep
      [ prettyRelevance y
        $ prettyHiding y parens
        $ prettyFiniteness (binderName $ namedArg y)
        $ prettyCohesion y
        $ prettyQuantity y
        $ prettyLock y
        $ prettyPolarity y
        $ prettyTactic (binderName $ namedArg y) $
        sep [ fsep (map (pretty . NamedBinding False) ys)
            , colon <+> pretty e ]
      | ys@(y : _) <- groupBinds $ List1.toList xs ]
      where
        groupBinds [] = []
        groupBinds (x : xs)
          | Just{} <- isLabeled x = [x] : groupBinds xs
          | otherwise   = (x : ys) : groupBinds zs
          where (ys, zs) = span (same x) xs
                same x y = getArgInfo x == getArgInfo y && isNothing (isLabeled y)

newtype Tel = Tel Telescope

instance Pretty Tel where
    pretty (Tel tel)
      | any isMeta tel = forallQ <+> fsep (map pretty tel)
      | otherwise      = fsep (map pretty tel)
      where
        isMeta (TBind _ _ (Underscore _ Nothing)) = True
        isMeta _ = False

smashTel :: Telescope -> Telescope
smashTel (TBind r xs e  :
          TBind _ ys e' : tel)
  | prettyShow e == prettyShow e' = smashTel (TBind r (xs <> ys) e : tel)
smashTel (b : tel) = b : smashTel tel
smashTel [] = []


instance Pretty RHS where
    pretty (RHS e)   = equals <+> pretty e
    pretty AbsurdRHS = empty

instance Pretty WhereClause where
  pretty  NoWhere = empty
  pretty (AnyWhere _ [Module _ NotErased{} x [] ds])
    | isNoName (unqualify x)
                       = vcat [ hlKeyword "where", nest 2 (vcat $ map pretty ds) ]
  pretty (AnyWhere _ ds) = vcat [ hlKeyword "where", nest 2 (vcat $ map pretty ds) ]
  pretty (SomeWhere _ erased m a ds) =
    vcat [ hsep $ privateWhenUserWritten a
             [ hlKeyword "module", prettyErased erased (pretty m), hlKeyword "where" ]
         , nest 2 (vcat $ map pretty ds)
         ]
    where
      privateWhenUserWritten = \case
        PrivateAccess _ UserWritten -> (hlKeyword "private" :)
        _ -> id

instance Pretty LHS where
  pretty (LHS p eqs es) = sep
    [ pretty p
    , nest 2 $ if null eqs then empty else fsep $ map pretty eqs
    , nest 2 $ prefixedThings (hlKeyword "with") (map prettyWithd es)
    ] where

    prettyWithd :: WithExpr -> Doc
    prettyWithd (Named nm wh) =
      let e = pretty wh in
      case nm of
        Nothing -> e
        Just n  -> pretty n <+> colon <+> e

instance Pretty LHSCore where
  pretty (LHSHead f ps) = sep $ pretty f : map (parens . pretty) ps
  pretty (LHSProj d ps lhscore ps') = sep $
    pretty d : map (parens . pretty) ps ++
    parens (pretty lhscore) : map (parens . pretty) ps'
  pretty (LHSWith h wps ps) = if null ps then doc else
      sep $ parens doc : map (parens . pretty) ps
    where
    doc = sep $ pretty h <$ fmap ((pipe <+>) . pretty) wps
  pretty (LHSEllipsis _ _) = "..."

instance Pretty ModuleApplication where
  pretty (SectionApp _ bs x es) = fsep $ concat
    [ map pretty bs
    , [ equals, pretty x ]
    , map pretty es
    ]
  pretty (RecordModuleInstance _ x) = equals <+> pretty x <+> "{{...}}"

instance Pretty DoStmt where
  pretty (DoBind _ p e cs) =
    ((pretty p <+> fromArrow) <?> pretty e) <?> prCs cs
    where
      prCs [] = empty
      prCs cs = hlKeyword "where" <?> vcat (map pretty cs)
  pretty (DoThen e)   = pretty e
  pretty (DoLet _ ds) = hlKeyword "let" <+> vcat (fmap pretty ds)

instance Pretty Declaration where
  prettyList = vcat . map pretty
  pretty = \case
    TypeSig i tac x e ->
      sep [ prettyTactic' tac $ prettyRelevance i $ prettyCohesion i $ prettyQuantity i $ prettyPolarity i $ pretty x <+> colon
          , nest 2 $ pretty e
          ]
    FieldSig inst tac x (Arg i e) ->
      mkInst inst $ mkOverlap i $
      -- We print relevance before hiding, need to clear it before printing the rest of the attributes with TypeSig.
      prettyRelevance i $ prettyHiding i id $
      pretty $ TypeSig (setRelevance relevant i) tac x e
      where
        mkInst (InstanceDef _) d = sep [ hlKeyword "instance", nest 2 d ]
        mkInst NotInstanceDef  d = d

        mkOverlap i d | isYesOverlap i = hlKeyword "overlap" <+> d
                      | otherwise      = d
    Field _ fs ->
      sep [ hlKeyword "field"
          , nest 2 $ vcat (map pretty fs)
          ]
    FunClause ai lhs rhs wh _ ->
      sep [ pretty (getModality ai)
          , pretty lhs
          , nest 2 $ pretty rhs
          ] $$ nest 2 (pretty wh)
    DataSig _ erased x tel e ->
      sep [ hsep  [ hlKeyword "data"
                  , prettyErased erased (pretty x)
                  , fsep (map pretty tel)
                  ]
          , nest 2 $ hsep
                  [ colon
                  , pretty e
                  ]
          ]
    Data _ erased x tel e cs ->
      sep [ hsep  [ hlKeyword "data"
                  , prettyErased erased (pretty x)
                  , fsep (map pretty tel)
                  ]
          , nest 2 $ hsep
                  [ colon
                  , pretty e
                  , hlKeyword "where"
                  ]
          ] $$ nest 2 (vcat $ map pretty cs)
    DataDef _ x tel cs ->
      sep [ hsep  [ hlKeyword "data"
                  , pretty x
                  , fsep (map pretty tel)
                  ]
          , nest 2 $ hlKeyword "where"
          ] $$ nest 2 (vcat $ map pretty cs)
    RecordSig _ erased x tel e ->
      sep [ hsep  [ hlKeyword "record"
                  , prettyErased erased (pretty x)
                  , fsep (map pretty tel)
                  ]
          , nest 2 $ hsep
                  [ colon
                  , pretty e
                  ]
          ]
    Record _ erased x dir tel e cs ->
      pRecord erased x dir tel (Just e) cs
    RecordDef _ x dir tel cs ->
      pRecord defaultErased x dir tel Nothing cs
    Infix f xs  ->
      pretty f <+> fsep (punctuate comma $ fmap pretty xs)
    Syntax n _xs -> hlKeyword "syntax" <+> pretty n <+> "..."
    PatternSyn _ n as p -> hlKeyword "pattern" <+> pretty n <+> fsep (map pretty as)
                             <+> equals <+> pretty p
    Mutual _ ds     -> namedBlock "mutual" ds
    InterleavedMutual _ ds  -> namedBlock "interleaved mutual" ds
    LoneConstructor _ ds -> namedBlock "data _ where" ds
    Abstract _ ds   -> namedBlock "abstract" ds
    Private _ _ ds  -> namedBlock "private" ds
    InstanceB _ ds  -> namedBlock "instance" ds
    Macro _ ds      -> namedBlock "macro" ds
    Postulate _ ds  -> namedBlock "postulate" ds
    Primitive _ ds  -> namedBlock "primitive" ds
    Generalize _ ds -> namedBlock "variable" ds
    Opaque _ ds     -> namedBlock "opaque" ds
    Unfolding _ rs  -> hlKeyword "unfolding" <+> braces (fsep (punctuate semi (pretty <$> rs)))
    Module _ erased x tel ds ->
      hsep [ hlKeyword "module"
           , prettyErased erased (pretty x)
           , fsep (map pretty tel)
           , hlKeyword "where"
           ] $$ nest 2 (vcat $ map pretty ds)
    ModuleMacro _ NotErased{} x (SectionApp _ [] y es) doOpen@(DoOpen _kwr) i
      | isNoName x ->
      sep [ pretty doOpen
          , nest 2 $ fsep $ pretty y : map pretty es
          , nest 4 $ pretty i
          ]
    ModuleMacro _ erased x (SectionApp _ tel y es) open i ->
      sep [ pretty open <+> hlKeyword "module" <+>
            prettyErased erased (pretty x) <+> fsep (map pretty tel)
          , nest 2 $ fsep $ concat [ [ equals, pretty y ], map pretty es, [ pretty i ] ]
          ]
    ModuleMacro _ erased x (RecordModuleInstance _ rec) open _i ->
      sep [ pretty open <+> hlKeyword "module" <+> prettyErased erased (pretty x)
          , nest 2 $ equals <+> pretty rec <+> "{{...}}"
          ]
    Open _ x i  -> hsep [ hlKeyword "open", pretty x, pretty i ]
    Import open _ x rn i   ->
      hsep [ pretty open, hlKeyword "import", pretty x, as rn, pretty i ]
      where
        as (Left x) = hlKeyword "as" <+> pretty (asName x)
        as (Right args) = fsep (map pretty args)
    UnquoteDecl _ xs t ->
      sep [ hlKeyword "unquoteDecl" <+> fsep (map pretty xs) <+> equals, nest 2 $ pretty t ]
    UnquoteDef _ xs t ->
      sep [ hlKeyword "unquoteDef" <+> fsep (map pretty xs) <+> equals, nest 2 $ pretty t ]
    UnquoteData _ x xs t ->
      sep [ hlKeyword "unquoteData" <+> pretty x <+> fsep (map pretty xs) <+> equals, nest 2 $ pretty t ]
    Pragma pr   -> sep [ "{-#" <+> pretty pr, "#-}" ]
    where
      namedBlock s ds =
          sep [ hlKeyword (text s)
              , nest 2 $ vcat $ map pretty ds
              ]

pHasEta0 :: HasEta0 -> Doc
pHasEta0 = \case
  YesEta   -> hlKeyword "eta-equality"
  NoEta () -> hlKeyword "no-eta-equality"

instance Pretty RecordDirective where
  pretty = pRecordDirective

pRecordDirective :: RecordDirective -> Doc
pRecordDirective = \case
  Induction ind -> pretty (rangedThing ind)
  Constructor n inst -> hsep [ pInst, hlKeyword "constructor", pretty n ] where
    pInst = case inst of
      InstanceDef{} -> hlKeyword "instance"
      NotInstanceDef{} -> empty
  Eta eta -> pHasEta0 (rangedThing eta)
  PatternOrCopattern{} -> hlKeyword "pattern"

pRecord
  :: Erased
  -> Name
  -> [RecordDirective]
  -> Parameters
  -> Maybe Expr
  -> [Declaration]
  -> Doc
pRecord erased x directives tel me ds = vcat
    [ sep
      [ hsep  [ hlKeyword "record"
              , prettyErased erased (pretty x)
              , fsep (map pretty tel)
              ]
      , nest 2 $ pType me
      ]
    , nest 2 $ vcat $ concat
      [ map pretty directives
      , map pretty ds
      ]
    ]
  where
    pType (Just e) = hsep [ colon, pretty e, hlKeyword "where" ]
    pType Nothing  = hlKeyword "where"

instance Pretty OpenShortHand where
    pretty = \case
      DoOpen _ -> hlKeyword "open"
      DontOpen -> empty

instance Pretty Pragma where
    pretty (OptionsPragma _ opts)  = fsep $ hlKeyword "OPTIONS" : map (hlPragma . text) opts
    pretty (BuiltinPragma _ b x)   = hsep [ hlKeyword "BUILTIN", hlPragma (text (rangedThing b)), pretty x ]
    pretty (RewritePragma _ _ xs)    =
      hsep [ hlKeyword "REWRITE", hsep $ map pretty xs ]
    pretty (CompilePragma _ b x e) =
      hsep [ hlKeyword "COMPILE", pretty (rangedThing b), pretty x, textNonEmpty e ]
    pretty (ForeignPragma _ b s) =
      vcat $ hsep [ hlKeyword "FOREIGN", pretty (rangedThing b) ] : map text (lines s)
    pretty (StaticPragma _ i) =
      hsep $ [hlKeyword "STATIC", pretty i]
    pretty (InjectivePragma _ i) =
      hsep $ [hlKeyword "INJECTIVE", pretty i]
    pretty (InjectiveForInferencePragma _ i) =
      hsep $ [hlKeyword "INJECTIVE_FOR_INFERENCE", pretty i]
    pretty (InlinePragma _ True i) =
      hsep $ [hlKeyword "INLINE", pretty i]
    pretty (NotProjectionLikePragma _ i) =
      hsep $ [hlKeyword "NOT_PROJECTION_LIKE", pretty i]
    pretty (InlinePragma _ False i) =
      hsep $ [hlKeyword "NOINLINE", pretty i]
    pretty (ImpossiblePragma _ strs) =
      hsep $ [hlKeyword "IMPOSSIBLE"] ++ map text strs
    pretty (EtaPragma _ x) =
      hsep $ [hlKeyword "ETA", pretty x]
    pretty (TerminationCheckPragma _ tc) =
      case tc of
        TerminationCheck       -> __IMPOSSIBLE__
        NoTerminationCheck     -> hlKeyword "NO_TERMINATION_CHECK"
        NonTerminating         -> hlKeyword "NON_TERMINATING"
        Terminating            -> hlKeyword "TERMINATING"
        TerminationMeasure _ x -> hsep $ [hlKeyword "MEASURE", pretty x]
    pretty (NoCoverageCheckPragma _) = hlKeyword "NON_COVERING"
    pretty (WarningOnUsage _ nm str) = hsep [ hlKeyword "WARNING_ON_USAGE", pretty nm, hlPragma (text (show str)) ]
    pretty (WarningOnImport _ str)   = hsep [ hlKeyword "WARNING_ON_IMPORT", hlPragma (text (show str)) ]
    pretty (CatchallPragma _) = hlKeyword "CATCHALL"
    pretty (DisplayPragma _ lhs rhs) = hlKeyword "DISPLAY" <+> sep [ pretty lhs <+> equals, nest 2 $ pretty rhs ]
    pretty (NoPositivityCheckPragma _) = hlKeyword "NO_POSITIVITY_CHECK"
    pretty (PolarityPragma _ q occs) =
      hsep (hlKeyword "POLARITY" : pretty q : map pretty occs)
    pretty (NoUniverseCheckPragma _) = hlKeyword "NO_UNIVERSE_CHECK"
    pretty (OverlapPragma _ x m) = hsep [pretty m, pretty x]

instance Pretty NotationPart where
    pretty (IdPart x) = text $ rangedThing x
    pretty HolePart{} = underscore
    pretty VarPart{}  = underscore
    pretty WildPart{} = underscore

    prettyList = hcat . map pretty

instance Pretty Fixity' where
    pretty (Fixity' fix nota _range)
      | null nota = pretty fix
      | otherwise = hlKeyword "syntax" <+> pretty nota

instance Pretty Pattern where
    prettyList = fsep . map pretty
    pretty = \case
            IdentP _ x      -> pretty x
            AppP p1 p2      -> sep [ pretty p1, nest 2 $ pretty p2 ]
            RawAppP _ ps    -> fsep $ map pretty $ List2.toList ps
            OpAppP _ q _ ps -> fsep $ prettyOpApp empty q $ fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps
            HiddenP _ p     -> braces' $ pretty p
            InstanceP _ p   -> dbraces $ pretty p
            ParenP _ p      -> parens $ pretty p
            WildP _         -> underscore
            AsP _ x p       -> pretty x <> hlSymbol "@" <> pretty p
            DotP _ _ p      -> "." <> pretty p
            AbsurdP _       -> "()"
            LitP _ l        -> pretty l
            QuoteP _        -> hlKeyword "quote"
            RecP _ _ fs     -> sep [ hlKeyword "record", bracesAndSemicolons (map pretty fs) ]
            EqualP _ es     -> sep $ for es \ (e1, e2) -> parens $ sep [pretty e1, equals, pretty e2]
            EllipsisP _ _   -> "..."
            WithP _ p       -> "|" <+> pretty p

prettyOpApp :: forall a .
  Pretty a => Asp.Aspects -> QName -> List1 (NamedArg (MaybePlaceholder a)) -> [Doc]
prettyOpApp asp q es = merge [] $ prOp ms xs $ List1.toList es
  where
    -- ms: the module part of the name.
    ms = List1.init (qnameParts q)
    -- xs: the concrete name (alternation of @Id@ and @Hole@)
    xs = case unqualify q of
           Name _ _ xs    -> List1.toList xs
           NoName{}       -> __IMPOSSIBLE__

    prOp :: [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Doc, Maybe PositionInName)]
    prOp ms (Hole : xs) (e : es) =
      case namedArg e of
        Placeholder p   -> (qual ms $ pretty e, Just p) : prOp [] xs es
        NoPlaceholder{} -> (pretty e, Nothing) : prOp ms xs es
          -- Module qualifier needs to go on section holes (#3072)
    prOp _  (Hole : _)  []       = __IMPOSSIBLE__
    prOp ms (Id x : xs) es       = ( qual ms $ annotate asp $ pretty $ simpleName x
                                   , Nothing
                                   ) : prOp [] xs es
      -- Qualify the name part with the module.
      -- We then clear @ms@ such that the following name parts will not be qualified.

    prOp _  []       es          = map (\e -> (pretty e, Nothing)) es

    qual ms doc = hcat $ punctuate "." $ map pretty ms ++ [doc]

    -- Section underscores should be printed without surrounding
    -- whitespace. This function takes care of that.
    merge :: [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
    merge before []                            = reverse before
    merge before ((d, Nothing) : after)        = merge (d : before) after
    merge before ((d, Just Beginning) : after) = mergeRight before d after
    merge before ((d, Just End)       : after) = case mergeLeft d before of
                                                   (d, bs) -> merge (d : bs) after
    merge before ((d, Just Middle)    : after) = case mergeLeft d before of
                                                   (d, bs) -> mergeRight bs d after

    mergeRight before d after =
      reverse before ++
      case merge [] after of
        []     -> [d]
        a : as -> (d <> a) : as

    mergeLeft d before = case before of
      []     -> (d,      [])
      b : bs -> (b <> d, bs)
